COMMENT ⊗   VALID 00011 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00009 00003	#. Reversing a list
C00014 00004	#. Non Algolic Elephant Programs
C00016 00005	#. An airline reservation system
C00020 00006	#. Elephant program to count vertices in a list structure
C00024 00007	#. Parallel processes for computing a sum of functions
C00030 00008	#. Remarks
C00035 00009	#. References
C00036 00010	.if false then begin
C00042 00011	.end
C00043 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source
.at "qg" ⊂"%3go_to%*"⊃
.at "qNIL" ⊂"%1NIL%*"⊃
.turn on "→"
.cb THE PROGRAMMING LANGUAGE ELEPHANT
.skip 1
.once center
by John McCarthy


	The Elephant (it never forgets) programming language
does assignment by regarding variables as explicit functions
of time; e.g. where Algol expects %2x :=%1, Elephant expects %2x(t) =%1.
The program counter is also explicitly regarded as a function of time.
Overcoming the inhibition against explicit use of time as the
independent variable allows programs to be represented as collections
of sentences in a first order logical language that can be used to
prove properties of the program.  Moreover, allowing the right hand
sides of equations to refer to other than the immediate past allows
"high level" programs that don't require data structure definitions
required by ordinary programming languages.
The concepts are best understood by means of examples.
The notation is as in (Cartwright and McCarthy 1979).

.item←0
#. Translating a sequential program into Elephant

	Consider the following Algol 60 program fragment (declarations
are omitted) for doing multiplication by addition:

.begin nofill
%2

	i := n;				∂(40)0
	p := 0;				∂(40)1
loop:	qif i = 0 qthen qg done;	∂(40)2
	i := i - 1;			∂(40)3
	p := p + m;			∂(40)4
	qg loop;			∂(40)5
done:					∂(40)6
.end

The corresponding Elephant program consists of the equations

.begin nofill
.zz←12
%2

pc(0) = 0,

∀t.[i(t+1) →=_∂(zz)IF pc(t) = 0 THEN n
∂(zz)ELSE IF pc(t) = 3 THEN i(t) - 1
∂(zz)ELSE i(t)],

∀t.[p(t+1) →=_∂(zz)IF pc(t) = 1 THEN 0
∂(zz) ELSE IF pc(t) = 4 THEN p(t) + m
∂(zz)ELSE p(t)],

%1and%2

∀t.[pc(t+1) →=_∂(zz)IF pc(t) = 2 ∧ i(t) = 0 THEN 6
∂(zz)ELSE IF pc(t) = 5 THEN 2
∂(zz)ELSE pc(t) + 1].
.end

	In these equations ⊗i(t) and ⊗p(t) replace the simple
variables of the Algol program.  The function ⊗pc(t) is the
program counter, and it takes values from 1 to 6, corresponding
to the numbers written on the right of the Algol program.  It should
be apparent from the example that any program made up of assignments
and qgs can be systematically translated to an Elephant program.
We have used the logical conditional expression %2IF_..._THEN_..._ELSE%1
rather than qif_..._qthen_..._qelse, because there is no reason to
provide for the undefined case.
Notice also that the length of the Elephant program is linear in the
length of the original program.

	Having one value of ⊗pc(t) for
each statement in the Algol program is unnecessary, although it makes
the systematic character of the translation more apparent.  If we
let %2pc(t)_=_0%1 correspond to the initialization, ⊗pc(t)_=_1 correspond
to the loop, and ⊗pc(t)_=_2 correspond to the label ⊗done, then the
equations become

.begin nofill
.zz←12
%2

pc(0) = 0,

∀t.[i(t+1) →=_∂(zz)IF pc(t) = 0 THEN n
∂(zz)ELSE IF pc(t) = 1 ∧ i(t) ≠ 0 THEN i(t) - 1
∂(zz)ELSE i(t)],

∀t.[p(t+1) →=_∂(zz)IF pc(t) = 0 THEN 0
∂(zz) ELSE IF pc(t) = 1 ∧ i(t) ≠ 0 THEN p(t) + m
∂(zz)ELSE p(t)],

%1and%2

∀t.[pc(t+1) →=_∂(zz)IF pc(t) = 1 ∧ i(t) = 0 THEN 2
∂(zz)ELSE pc(t) + 1].
.end

	The correctness of the original Elephant program is given by the
sentence

	%2∀m n ∃t.[pc(t) = 6 ∧ p(t) = mn]%1,

while the modified program would have the same correctness condition
except for having ⊗pc(t)_=_2 instead of ⊗pc(t)_=_6.  Either statement
is provable from the any first order axiomatization of arithmetic
together with the sentences constituting the program.  No special
axioms for programs or "logic of programs" is required.

	Thus an entirely conventional mathematical way of writing
recursion equations leads to a convenient programming language.  I
am tempted to call the language Algol 50, since it could easily have
been developed at that time.

	The proof of correctness for this
multiplication program is misleadingly simple, since
we can easily write explicit formulas for ⊗i(t), ⊗p(t), and
⊗pc(t) and prove them by mathematical induction.  More typical proofs
occur when it isn't convenient to give explicit formulas for the
variables as functions of time or for the value of ⊗t for which the
program terminates.  Then the computational content of the proof is
is often essentially the same as that of an %2inductive assertions%1 proof
combined with induction on a rank function of the variables taking
values in a suitable inductively ordered set.

#. Reversing a list

	Reversing a list provides another example of an Elephant program
and a proof of its correctness.
.skip to column 1
.begin nofill
%2
	u := w;
	v := qNIL;
loop:	qif qn u qthen qg done;
	v := [qa u] . v;
	u := qd u;
	qg loop;
done:
.end

	The corresponding Elephant program is

.begin nofill
%2
.zz←12

pc(0) = 0,

∀t.[u(t+1) →=_∂(zz)IF pc(t) = 0 THEN w
		∂(zz)ELSE IF pc(t) = 1 ∧ ¬null u(t) THEN qd u(t)
		∂(zz)ELSE u(t)],

∀t.[v(t+1) →=_∂(zz)IF pc(t) = 0 THEN qNIL
		∂(zz) ELSE IF pc(t) = 1 ∧ ¬null u(t) THEN qa u(t) . v(t)
		∂(zz) ELSE v(t)]

∀t.[pc(t+1) →=_∂(zz)IF pc(t) = 1 ∧ ¬null u(t) THEN 1
		∂(zz)ELSE pc(t) + 1].
.end

	In order to give the specifications for this program, we will
use the LISP program ⊗reverse defined by

	%2reverse u ← qif qn u qthen qNIL qelse reverse qd u * <qa u>%1.

With the latter, as shown in (Cartwright and McCarthy 1979), it is
convenient to prove such properties as %2reverse_reverse_u_=_u%1 and
%2reverse[u_*_v]_=_reverse_v_*_reverse_u%1.  The major fact about
the Elephant program is expressed by

	%2∃t.(pc(t) = 2 ∧ v(t) = reverse w)%1.

It can be proved by proving that %2length u(t)%1 is a decreasing function
of ⊗t, i.e. for any ⊗t such that ⊗pc(t)_<_2, there is %2t'_>_t%1 such
that %2length_u(t')_<_length_t%1, and also that

	%2∀t.[reverse_w = reverse u(t) * v(t)]%1.

This is just an %2inductive assertions%1 proof.  So far it seems that
the our Elephant technique of proof is essentially %2inductive assertions%1,
and is less flexible than the technique described in (Cartwright and
McCarthy 1979) that uses the %2functional equation%1 and the %2minimization
schema%1.  This is because %2inductive assertions%1 provides no way
of expressing algebraic relations among functions defined by programs.

	One mathematically straightforward way of defining functions by
programs is the following.  We rewrite the above equations to introduce
⊗w as an explicit argument of the functions so that they become ⊗u(t,w), 
⊗v(t,w), and pc(t,w).  We then define a relation ⊗reverses(v,w) by

	%2∀v w.(reverses(v,w) ≡ ∃t.(pc(t,w) = 2 ∧ v(t,w) = v))%1.

When we have proved %2∀w ∃!v.reverses(v,w)%1, first order logic
entitles us to replace the relation ⊗reverses by a function.  We can
then prove successivel that this function satisfies the relations

	%2reverse qNIL = qNIL%1,

	%2reverse [x . u] = reverse u * <x>%1

	%2reverse reverse u = u%1,

and

	%2reverse[u * v] = reverse v * reverese u%1,

where the notation is as in (McCarthy and Talcott 1979).

#. Non Algolic Elephant Programs

	When we translate an Algol program into Elephant, we get
equations in which the %2x(t+1)%1s depend only on the %2x(t)%1s.
However, the recursion
equations will still have guaranteed solutions if the %2x(t)%1s depend on
arbitrary earlier values of ⊗t.  This leads to a "high level" programming
language with the following features:

	1. The program refers to the past through earlier values of
⊗t, just as though everything were remembered.  That's why we call
the language Elephant.

	2. The compiler is smart and decides what data structures are
required in order to carry out the computations without remembering
everything.  To the extent that compilers can be written that do this
effectively, Elephant is a "higher level" language in which the
programer specifies less than in Algol, etc.

#. An airline reservation system

	Consider programming a trivial airline reservation system.
We want to say that %2a passenger has a reservation if he
has made one that has not been cancelled%1.  We do not want to prescribe
what data structures have to be kept in order to be able to answer the
question of whether someone has a reservation.

	This program replies properly to requests to make reservations,
cancel them, and to inquiries about whether a reservation exists.
The program refers to its input in
terms of an abstract analytic syntax the meaning of whose mnemonic
predicate and function names is hopefully obvious.  The only data
structure explicitly mentioned is the number of seats currently occupied,
and even that could be eliminated from the program.  The Elephant compiler,
therefore, gets the honor of figuring out what other data structures
are needed.  We use the convention of writing %2α{xα}f%1 instead of ⊗f(x) when
it is convenient to write the argument before the function name.
.begin nofill
.uu←35

%2
∀t.[output(t+1) = α{input(t)α}[λ in.
∂(10)IF ismake in THEN →[∂(uu)IF hasrev(maker in,t) THEN "You had it"
			∂(uu)ELSE IF number(t) = N THEN "No room"
			∂(uu)ELSE "You have it now"]
∂(10)ELSE IF iscancel in THEN →[∂(uu)IF hasrev(maker in,t) THEN "It's cancelled"
			∂(uu)ELSE "You don't have it to cancel"]
∂(10)ELSE IF isinquiry in THEN→[∂(uu)IF hasrev(maker in,t) THEN "You have one"
			∂(uu)ELSE "You don't have one"]
∂(10)ELSE qNIL]

∀t.[number(t+1) = α{input(t)α}[λ in.
∂(10)IF ismake in THEN →[∂(uu)IF hasrev(maker in,t) ∨ number(t) = N
∂(uu)THEN number(t)
∂(uu)ELSE number(t) + 1]
∂(10)ELSE IF iscancel in THEN →[∂(uu)IF hasrev(maker in,t) THEN number(t) - 1
			∂(uu)ELSE number(t)]
∂(10)ELSE number(t)]
.end

where

	%2∀t.[hasrev(passenger,t) ≡ ∃t1.(t1 < t ∧ ismake input t1 ∧
passenger = maker input t1 ∧ number(t1) < N) ∧ ¬∃t2.(t1 < t2 < t ∧
iscancel input t2 ∧ maker input t2 = passenger))]%1.

	The main difficulty in making a compiler for Elephant is illustrated
by the predicate ⊗hasrev.  The compiler has to understand that it
must remember successful reservations but can forget unsuccessful
attempts at making a reservation and that it can forget reservations
that have been cancelled.  Perhaps ⊗hasrev should be written using primitives
that refer explicitly to the most recent occurrence of an event,
which might permit a less intelligent compiler.

#. Elephant program to count vertices in a list structure

	Another context in which it is possible to avoid specifying a
data structure by referring to the past, occurs when a list structure
is to be scanned.  The simplest example is a program to count the
vertices in a list structure.

Here ⊗a is the list structure being scanned, ⊗x is a running variable for
the current structure, and ⊗n is the current count.

	Because of Elephant's ability to refer to the past, we can
write this program without specifying a stack.  It is up to the compiler
to decide that a stack is appropriate for implementing the algorithm.

.begin nofill
%2 
∀t.[x(t+1) →=_∂(16)IF pc(t) =_0 THEN a
∂(16)ELSE IF pc(t) =_1 THEN
→[∂(22)IF [∀y.seen(y,t) ⊃ atom y ∨ seen(car y,t) ∧ seen(cdr y, t)]
∂(30)THEN x(t)
∂(22)ELSE IF ¬atom x(t) ∧ ¬seen(car x(t),t) then car x(t)
∂(22)ELSE cdr x(mostrecent(t,λt1.¬seen(cdr(x(t1)),t)))]
∂(16)ELSE x(t)]

∀t.[n(t+1) →=_∂(16)IF pc(t) =_0 THEN 0
∂(16)ELSE IF ∂(25)pc(t) =_1 
→∧ ∂(25)¬[∀y.seen(y,t) ⊃ atom y ∨ seen(car y,t) ∧ seen(cdr y, t)]
∂(30)THEN n(t) + 1
∂(16)ELSE n(t)]

∀t.[pc(t+1) →=_∂(16)IF ∂(20)pc(t) =_1
→∧ ∂(20)¬[∀y.seen(y,t) ⊃ atom y ∨ seen(car y,t) ∧ seen(cdr y, t)]
∂(25)THEN 1
∂(16)ELSE pc(t) + 1
.end

where the predicate ⊗seen and the functional ⊗mostrecent are defined as
follows:
.begin nofill
%2 
∀y t.[seen(y,t) ≡ ∃t1.[t1 ≤ t ∧ y =_x(t1)]]

∀t.[mostrecent(t, pred) = qif pred t qthen t qelse mostrecent(t - 1, pred)].
.end

We would like to regard these as definitions not as programs.  Indeed the
compiled program shouldn't compile them directly, but should do the job
another way that uses time and space more efficiently.

Of course, this example is less perspicuous than the lisp program

%2count x ← qif qat x qthen 1 qelse count qa x + count qd x%1

which scans the vertices in the same order.  But then this problem
is especially appropriate for recursion and Lisp's built-in stack
mechanism.

Most likely ⊗seen and ⊗mostrecent will occur in other algorithms
where one doesn't want to look at things that have been already tried.

#. Parallel processes for computing a sum of functions

.begin
.turn on "[]↑↓&"
.font B "BDJ20"

	The following is an Elephant program to compute %AS%B↑N&↓[n=1]%2f(n))%1
using ⊗k processors.  A master processor
initializes the variables ⊗n and ⊗s and starts the ⊗k slave
processes at step 1.  A process needs exclusive access to ⊗n when
it is reading it and incrementing it, and it needs exclusive access
to ⊗s when incrementing it, and we only provide for exclusive access
at these times.  We imagine that computing ⊗f(n) takes ⊗time(n) units
of time, and these operations are done in parallel.  ⊗pc(t) is the
program counter for the master process, and ⊗pc(i,t) is the program
counter of the %2i%1th slave process.  The updating of all variables
except the ⊗pc(i,t) works as in Algolic programs, but the latter
requires a more elaborate description.
.end

.begin nofill
.ww←10
%2 

n(t+1)→=_∂(ww)IF pc(t) = 0 THEN 1
∂(ww)ELSE IF pc(i,t) = 1 ∧ n(t) ≤ N THEN n(t) + 1
∂(ww)ELSE n(t)

s(t+1)→=_∂(ww)IF pc(t) = 0 THEN 0
∂(ww)ELSE IF pc(i,t) = 5 THEN s(t) + m(i,t)
∂(ww)ELSE s(t)

m(i,t+1)→=_∂(ww)IF pc(i,t) = 2 ∧ n(t) ≤ N THEN n(t)
∂(ww)ELSE IF pc(i,t+1) = 4 THEN f(m(i,t))
∂(ww)ELSE m(i,t)

pc(t+1) →=_∂(ww)IF pc(t) = 1 ∧ ∃i.(pc(i,t) ≠ 0) THEN 1
∂(ww)ELSE pc(t) + 1


pc(i,0) = 0

pc(i,t) = 0 ⊃ pc(i,t+1) = IF pc(t) = 0 THEN 1 ELSE 0

pc(i,t) = 1 ⊃ ∃!j.(pc(j,t) = 1 ∧ pc(j,t+1) = 2) ∧ ∃t'.(t < t' ≤ t+k ∧ pc(i,t') = 2)

pc(i,t) = 1 ⊃ pc(i,t+1) = 1 ∨ pc(i,t+1) = 2

pc(i,t) = 2 ⊃ pc(i,t+1) = IF n(t) ≤ N THEN 3 ELSE 0

pc(i,t) = 3 ∧ pc(i,t-1) ≠ 3 
∂(ww)⊃ ∀t'.(t ≤ t' < t + time(m(i,t)) ⊃ pc(i,t') = 3) ∧ pc(t+time(m(i,t))) = 4

pc(i,t) = 4 ⊃ ∃!j.(pc(j,t) = 4 ∧ pc(j,t+1) = 5) ∧ ∃t'.(t < t' ≤ t + k ∧ pc(i,t') = 5)

pc(i,t) = 5 ⊃ pc(i,t+1) = 1
.end

	It may be questioned whether the above Elephant program should be
regarded as a "program" that can be compiled by a suitable compiler or as
something between a specification and a program.  Perhaps it is an example
of that elusive concept called an algorithm.  Notice that it assumes that
synchronization occurs without specifying any way of doing it.  Just the
thing to challenge a smart compiler or automatic programming system.  On
the other hand, the correctness of the Elephant program is given by the
statement,

.begin nofill
.turn on "[]↑↓&"
.font B "BDJ20"

%2∃t.(pc(t) = 2 ∧ ∀i(pc(i,t) = 0) ∧ s(t) = %AS%B↑N&↓[n=1]%2f(n))%1
.end

and this can presumably be proved from the program.  The correspondence
between this Elephant program and one that is more explicit about
synchronization might be proved separately.

	There may well be better ways of describing parallel processes
in Elephant.

#. Remarks

1. Programs in Lucid (Ashcroft 1974) are also collections of sentences 
in a first order language.  A Lucid object is a vector of the values 
of a variable throughout time.  This permits some statements to be
made in a very neat way.  However, it seems to be less flexible than
the Elephant device of admitting the time as an explicit parameter.
Lucid program do not admit qgs, and there are other unexpected
restrictions.

2. The properties of Elephant programs don't depend on time taking
integer values.  All we need require is that the set of times be ordered
and unbounded above.  Then the first sentence of the product program
would take the form
.begin nofill
.u←20

%2∀t ∃t'.[t' > t ∧ i(t') →=_∂uIF pc(t) = 0 THEN n
∂uELSE IF pc(t) = 3 THEN i(t) - 1
∂uELSE i(t)].
.end

#. References

%3Cartwright, Robert and John McCarthy (1979)%1: "Recursive Programs
as Functions in a First Order Theory", in %2
.if false then begin
Notes

1979 March 30

What concept of equivalence of Elephant programs should be used?

What should be proved about airline program?

Another example where data structure is not specified?
Maybe topological sort?
(General example: do not treat an item that has been previously treated)

Can elephant idea be extended to interacting parallel programs?

1979 March 31

Suppose a function is computed by an elephant program.  How does one
define the function and prove its properties?  Example: append or reverse.

How is a program equivalent to one which is obtained from it by
introducing a new variable and computing it?  We need a concept of
equivalence of programs w/r set of variables.  

Parallel programs

	Consider the following Algolic program in which two processes
co-operate in finding the largest element of an array.

.begin nofill
%2 
∂9n := 1; b := 0;	∂(40)0
∂9qg l1,l2;∂(40)1
l1:∂9if n = N qthen qg done;∂(40)2
∂9b := max(b,a[n]);∂(40)3
∂9n := n + 1;∂(40)4
∂9qgl1;∂(40)5

l2:∂9if n = N qthen qg done;∂(40)2
∂9b := max(b,a[n]);∂(40)3
∂9n := n + 1;∂(40)4
∂9qgl2;∂(40)5

done:∂(40)6
.end

The intent is that the two programs share the variables ⊗b and ⊗n and
merge when they reach ⊗done.  It is also important that they not
interfere with each other.  We can describe this process using
the ideas of Elephant as follows:


.end
.SKIP 1
This partial draft of ELEPHA[S79,JMC] compiled at {time} on {date}.